fix: Java --unicode-char mode coercion improvements #3630
Merged
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This solution uses an AutoGeneratedToken when filling in an omitted size. Previously, the code looked at the LiteralExpr in ArrayDimensions[0], which had the effect of also eliding a programmer-supplied size. Also, the previous implementation would crash if a size was given but wasn’t a LiteralExpr.
* Remove duplicate check * Add omitted check * Change error message to talk about “memory limit” rather than some C# property
…a-unicode-char-improvements # Conflicts: # Source/DafnyCore/Compilers/GoLang/Compiler-go.cs # Source/DafnyCore/Compilers/Java/Compiler-java.cs # Source/DafnyCore/Compilers/Python/Compiler-python.cs # Source/DafnyCore/Compilers/SinglePassCompiler.cs # Source/DafnyRuntime/DafnyRuntime.py # Source/DafnyRuntime/DafnyRuntimeGo/DafnyRuntime.go # Test/unicodechars/comp/Arrays.dfy # Test/unicodechars/comp/Arrays.dfy.expect
…a-unicode-char-improvements
RustanLeino
requested changes
Feb 24, 2023
| @@ -1339,7 +1347,8 @@ protected class ClassWriter : IClassWriter { | |||
| } else if (member is Function fn) { | |||
| var wr = new ConcreteSyntaxTree(); | |||
| EmitNameAndActualTypeArgs(IdName(member), TypeArgumentInstantiation.ToActuals(ForTypeParameters(typeArgs, member, false)), member.tok, wr); | |||
| if (typeArgs.Count == 0 && additionalCustomParameter == null) { | |||
| // TODO: needs to check for argument conversions as well | |||
There was a problem hiding this comment.
Did you intend to act on this TODO in this PR? If not, I suggest adding a failing test case to Test/wishlist or somewhere.
There was a problem hiding this comment.
I intended to leave it for now, but you're right a negative test would be a good idea. But I think it's just easier to implement this too - it's a fluke that Arrays.dfy exposed the return value problem, I should really add dedicated tests for this in something like Strings.dfy instead.
| @@ -1367,7 +1376,15 @@ protected class ClassWriter : IClassWriter { | |||
| } | |||
| prefixWr.Write(") -> "); | |||
| wr.Write(")"); | |||
| return EnclosedLvalue(prefixWr.ToString(), obj, $".{wr.ToString()}"); | |||
|
|
|||
| // TODO: Need to check arguments as well. Probably could use something like EmitCoercionIfNecessary | |||
There was a problem hiding this comment.
Did you intend to act on this TODO in this PR? If not, I suggest adding a failing test case to Test/wishlist or somewhere.
There was a problem hiding this comment.
As above, fixed the gap instead.
|
This PR fixes #3413, right? |
…/dafny into java-unicode-char-improvements
…/dafny into java-unicode-char-improvements
RustanLeino
approved these changes
Feb 27, 2023
robin-aws
added a commit
that referenced
this pull request
Feb 27, 2023
Picking up recent changes from master, especially #3630 as those fixes are necessary to unblock #3635. <small>By submitting this pull request, I confirm that my contribution is made under the terms of the [MIT license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small>
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Fixes #3413.
Addresses the issues uncovered during #2818 by adding a
--unicode-charmode version ofTest/comp/Arrays.dfy, which all stem from incomplete handling of manual boxing/unboxing of theCodePointtype at various Java code generation points. Note this is still incomplete as there must be other spots that do not handle coercion correctly in general, but these changes at least coverArrays.dfy.It turned out that handling arrow coercion as in the Go compiler was not necessary for Java, because the initial casting of a function reference as a lambda is where the necessary boxing/unboxing needs to happen instead anyway. That is, a reference to a Dafny
function f(x: char): charhas to end up as a JavaFunction<CodePoint, CodePoint>and therefore be eta expanded from the start.Also removed the fail-fast behavior from
%testDafnyForEachCompileras I found it more useful for debugging that way.Also implemented
ConcreteSyntaxTree.Commaas part of an initial implementation of Java arrow conversion, which ended up not directly used but seems useful enough to keep (and I refactored one spot to use it as an example).Edit: I've also added a few more similar cases exposed as part of enabling
/unicodeChar:1by default for Dafny 4.0: #3635By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.